Sketches and Model Theory
15:01 Alright, everyone who's here might as well be here 15:01 So let's begin. 15:01 This seminar doesn't really overlap very much with the last one on model theory. 15:02 But we'll be doing things analogous to what we did before, so let's recap for like ten seconds. 15:02 First thing, we need a signature, a way of knowing what operations our theory has available. 15:02 It has constant symbols, function symbols, and relation symbols 15:03 So the theory of groups will have a signature of (1, *, ^-1) 15:03 or maybe (0, +, -) 15:03 the symbols themselves don't matter 15:03 all that matters is whether they're functions or relations 15:03 and how many arguments they take. 15:04 So fixing a signature, we can write down first-order sentences, defining them inductively 15:04 first terms as strings of symbols from the signature, with variables 15:04 then relations of terms, and the special relationship of model-equality a = b 15:05 and then quantified sentences, using Ax[ ... ] and Ex [ ... ] (which are my symbols today) 15:05 We select some of these sentences to be axioms; their deductive closure constitutes a 'theory' 15:06 The theory of groups is the set of all sentences that can be deduced from the group axioms. 15:06 A model of that theory is a set that interprets the signature of the theory, providing functions to function symbols and relations to relation symbols 15:07 Z_2 is a model of the theory of groups because it has 0 for 0, + mod 2 for +, and x + 1 mod 2 for -x. 15:07 Further, we say it's a model of the theory of groups because we we interpret those axioms within the model, they hold true. 15:08 Now, classical group theory (meaning pre-70's) took as its external theory normal set theory 15:08 That means when we're talking about models, we use the language of set theory 15:09 I don't want to talk about foundations very much, but I saw an estimate once that to do real model theory, you probably need about three uncountable ordinals, or something like that 15:09 ... that sounds like a lot. 15:10 So with the invention of category theory, there should be a way to shift paradigms, to be all witty and postmodern-sounding, and rewrite this stuff using CT-concepts 15:10 Now, my CT isn't so sharp, so you may have to warn me if I say something obviously not true. 15:10 in the late 60's, a guy named Ehresmann came up with a way of doing this using what he called (in French) sketches. 15:11 You can find a few of his papers on Numdam, but they're in french and difficult to understand. 15:11 Luckily, Wells and Barr took pity on us monolingual Americans and wrote a couple papers on the subject 15:11 Along with a few other people, like Makkai and some other guy I can't remember. 15:12 That's basically how I learned about sketches, and all that I know about them. My CT isn't strong enough to understand the big theorems, so today I want to sketch (har har) some examples of sketches 15:12 and show how you get the same expressiveness that you do with the set-theoretical language 15:13 so any questions about that before we start up? 15:13 Alright. 15:13 So first we need a category-analog of a signature. 15:14 Lawvere had a good idea, called the full clone. 15:14 This only works for signatures that only have functions; but that's not a big deal. 15:14 You start with the category whose objects are the natural numbers 15:15 Then you add an arrow from n to 1 if there's a function with arity n in the signature. 15:15 ! 15:15 Yo 15:15 DiffyQ: 15:15 One arrow per function or just one if there are any functions at all? 15:15 One arrow per function. 15:15 Cool. Carry on. 15:15 So in the group example you have an arrow 2 -> 1, an arrow 1 -> 1, and an arrow 0 -> 1 (for the identity) 15:16 Then, you add arrows for projections and injections, as if all the numbers were secretly powers of some object X 15:16 \(a, b) -> a, stuff like that 15:17 Finally, you add identity arrows, and closure under composition, and you've got yourself a category 15:17 You can take functors from this category to special categories whose objects are all products of some object X, and even get a sort of model theory out of it 15:17 but it's kind of unwieldy. 15:18 So the idea is to get rid of all the junk that had to get added on to make the full clone into a category. 15:18 What happens to a category when you take away composite arrows and identity arrows? 15:18 anyone 15:18 <_llll_> directed graph 15:19 right 15:19 So what Barr calls a trivial sketch is just going to be a directed graph 15:19 The objects of this directed graph are going to represent, in a way, the sorts of the theory 15:19 I don't know if sorts are really the same thing as types, but I think the word type is better known 15:20 Most familiar theories only have one basic type, but to get functions of higher arity you need products of that type 15:20 But perhaps I'm getting ahead of myself. Let's go back to that directed graph. 15:20 ! 15:20 The simplest directed graph has one node and no edges. 15:21 koeien: 15:21 so the directed graph we are talking about contains the arrows of the functions + the projections/injections, or were the last also thrown away? 15:21 Yeah, we threw everything away. 15:21 so only the functions (3 in the case of group theory) 15:21 Right now let's just talk about what the nodes are. 15:21 ok 15:21 thanks 15:22 To get to group theory, we'll need something more sophisticated than a directed graph. 15:22 Okay, so we have a single type, X. It's the only node, and there aren't any edges. 15:22 We want a functor-like thing from this graph to the category of sets to be a model for this sketch 15:23 The same way we had a function-like thing called interpretation from symbols to sets 15:23 We can't use functors, because a sketch isn't a category, and if we make it a category we'll be toting around N and a bunch of useless projections 15:24 So instead we make Set forget that it's a category, and call a 'sketch morphism' a graph homomorphism from a sketch to the underlying graph of the category of sets. 15:24 So nodes go to sets, and edges go to arrows pointing the same way. 15:25 For the sketch with one node and no edges, a model, i.e., a sketch morphism into Set, just picks out a special set from Set. 15:25 sets are surely models for the theory of sets. 15:25 Which is what the one-node sketch sketches. 15:25 A better sketch has two nodes, NODE and EDGE, and two arrows, EDGE --source--> NODE and EDGE --target--> NODE 15:26 If you follow a sketch morphism of this graph into Set, you find two sets with two parallel functions, i.e., a model of graphs 15:26 *directed graphs 15:26 This is great, but we don't have a way to make axioms hold true. 15:27 In CT, equations tend to be replaced with commutative diagrams 15:27 So lets enlarge our notion of a sketch to include some other diagrams 15:27 And enlarge our notion of sketch morphism to force these diagrams to map to commutative diagrams in the graph of the category. 15:29 We only require sketch morphisms to be one way, from the sketch to the underlying graph of the category. 15:30 And the image of a diagram in a sketch under this sketch morphism has to map to a commutative diagram in the category. 15:30 For example, we can add to the sketch of graphs an extra arrow EDGE --flip--> EDGE 15:31 together with a diagrams saying source . flip = target, target . flip = source, and flip . flip = id 15:32 This gives us the sketch of directed graphs where every edge has another edge that reverses it 15:32 I guess you'd call them self-dual directed graphs, or something. 15:32 It's kind of an artificial example. 15:32 <_llll_> i think you'd just call that "a graph" 15:32 Eh, there are more edges than there should be 15:33 I feel like you'd have to have some sort of equivalence relation ... I dunno. 15:33 Anyway. 15:34 What we have so far gives us the model theory of multi-sorted, linear, equational theories 15:34 multi-sorted because we can have more than one type, like we did with nodes and edges 15:34 linear because all the functions are 1-arity, and there aren't any relations. 15:34 We want n-arity functions, and to get that we need products of types. 15:35 From what little CT I know, a product is just a cone over a diagram that doesn't have any edges. 15:35 So that's exactly the data that we'll add to our notion of a sketch, and we'll force sketch morphisms to take those discrete cones to limit cones in the category. 15:35 Now my examples get even worse :) 15:35 ! 15:36 DiffyQ: 15:36 So do we require the categories we map into to have limits? 15:36 Or are we just doing Set? 15:36 All I really know is Set 15:36 Well that certainly has limits. 15:36 I know they do it to other categories, like Top 15:36 does that have the right limits? 15:37 It has products, modulo choice 15:37 It always has products. They might just be empty without choice. 15:37 <_llll_> yes, and pretty much every "big" category you'd want will have all limits 15:37 So, yeah, it's fine, go on. 15:37 Okay. 15:38 If these cones are also finite, you get what are called finite-product sketches 15:38 My horrible example of these are magmas, with signature (*) and no salient properties :) 15:39 You have a diagram with one node, X; together with a product cone X <- X2 -> X, and an arrow X2 -> X for the multiplication. 15:39 models of this have to map X2 to the X x X, so all is right with the world. 15:40 You can add on to this, X3 for an associativity square 15:40 X0 = 1 for constants 15:40 and even more diagrams, and eventually get a diagram for the theory of groups 15:40 ! 15:40 DiffyQ: 15:40 How does X0 work? 15:40 empty cone 15:40 Oh, durr. Okay. 15:41 Confused me too :) 15:41 I won't walk through that because it's a bit of effort to get all the right projections 15:41 So it just goes to the terminal object? 15:41 Yeah, like the definition of a group object (I think) 15:42 I.e., under no conditions, there's a unique map from anything to X0, which is what the empty cone would say. 15:42 Right 15:42 Err, the image of X0. 15:42 I understood what you meant. 15:42 In Set, that'll map to the singleton, which in turn will pick out whatever element of X is the identity 15:43 ! 15:43 antonfire: 15:43 So if you use Top instead of Set with the same sketch, do you get topological groups right away? 15:43 That's what I've been told. 15:43 That's neat. 15:43 <_llll_> yes, you're just doing group objects at this poitn 15:44 right. 15:44 FP-sketches will get you the multi-sorted equational theories, but that leaves out a lot of things 15:44 notably, fields 15:45 Right? multiplicative inverse over a field is a partial function, so it can't be done equationally. 15:45 <_llll_> 1!=0 in a field too 15:45 Good point. 15:46 So the way I tend to believe this is like this 15:46 If we restrict ourselves to the non-zero parts of a field, everything is well defined 15:46 so what we need to do is paste that zero on there 15:47 And the way they seem to do this is by writing the type of the field as the sum F = I + Z 15:47 F is the type of the field, I is the invertible elements, and Z is zero 15:47 Now to get that sum, you need discrete cocones, and doing a similar thing to the definition of a sketch and sketch morphism, you make the cocone diagrams go to limit cocones 15:48 A sketch with discrete, finite cocones is called a finite limit sketch, and it will get you the whole shebang of typical algebra. 15:49 Now you'll notice we actually have four definitions of a sketch, and there's a bunch of others 15:49 To make sure the definitions are right, they tend to call them doctrines. 15:49 So people talk about the finite product doctrine, or the finite limit doctrine, and so on. 15:50 And that's the limit of my knowledge of sketches at the moment. I'm still working on catching my CT up to snuff. 15:50 So feel free to ask embarassing questions that I can't answer :) 15:50 If you're interested, I can tar up the papers I have, though they're all available on various people's websites. 15:51 <_llll_> it would be nice to see how the field thing works, handling fields is iirc something you just Don't Do in universal algbera type formulations 15:51 I could draw it out if given enough time. 15:52 I'll see if I can get a scan of it with the seminar notes 15:52 There's also several different field sketches, and only one of them is good for topological fields, or so Barr says in I think Toposes, Triples, and Theories. 15:53 <_llll_> also, presumably there s a category of sketches (or doctrinres), so you could do sketches into the underlying set of Sketch (or Doctrince) 15:53 I'm pretty sure that's how they recover a definition for model equivalence 15:54 <_llll_> err, underlying catgeory, not underlying set 15:54 Natural transformations between such and such functors 15:54 I really need to learn more CT :( 15:55 <_llll_> i guess another question is why we should bother with all this, ok so a model for set theory is a sketch into Set, but you already had to have a "Set" there 15:55 <_llll_> but then i guess being able to fit fields into the same formualtion is worth soething 15:56 The equational way of doing things is really annoying sometimes. 15:56 The point, I think, is to be able to do model theory in a categorical framework. 15:56 <_llll_> but why is doing something in a categorical framework a sensible goal? 15:57 My motivation is the syntactic sugar 15:57 I dunno, I thought it was neat Category:Seminar Category:Model Theory